Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	app(app(fmap,fnil),x)	→ nil
2:	app(app(fmap,app(app(fcons,f),t)),x)	→ app(app(cons,app(f,x)),app(app(fmap,t),x))

There are 5 dependency pairs:


3:	APP(app(fmap,app(app(fcons,f),t)),x)	→ APP(app(cons,app(f,x)),app(app(fmap,t),x))
4:	APP(app(fmap,app(app(fcons,f),t)),x)	→ APP(cons,app(f,x))
5:	APP(app(fmap,app(app(fcons,f),t)),x)	→ APP(f,x)
6:	APP(app(fmap,app(app(fcons,f),t)),x)	→ APP(app(fmap,t),x)
7:	APP(app(fmap,app(app(fcons,f),t)),x)	→ APP(fmap,t)

The approximated dependency graph contains one SCC: {3,5,6}.

Tyrolean Termination Tool (0.02 seconds) --- May 3, 2006